-
Notifications
You must be signed in to change notification settings - Fork 18
/
FirstSchema1.scala
37 lines (28 loc) · 1.65 KB
/
FirstSchema1.scala
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
package gapt.examples
import gapt.expr._
import gapt.proofs.context.update.InductiveType
import gapt.proofs.context.update.Sort
import gapt.proofs.gaptic._
object FirstSchema1 extends TacticsProof {
//These are the two fundamental additions to the context needed for Schematic
//proof construction.
ctx += InductiveType( "nat", hoc"0 : nat", hoc"s : nat>nat" ) //defines the natural numbers
ctx += Sort( "i" ) //defines the first order term sort
// Note that at this point both sorts are empty (though in the case of the type "nat"
// we do have the individuals 0, s(0), s(s(0)), and so on, but no predicates or
//additional function symbols). We need to add constants, functions,
// and predicate symbols individually to the sorts. The above declarations
// only provide the particular types this objects can have but not the
// individuals of these types.
// Let us consider the "i" as a numeric sort but with different symbolism than the
// sort "nat" which will represent true natural numbers.
ctx += hoc"z:i" //This is the Zero for the "i" sort
ctx += hoc"g:i>i" //This is the Successor for the "i" sort
// the hoc prefix on the two strings tells us that these are higher-order constants
// the type of these constants is represented by the :i and :i>i . As one can guess
// z is a constant and g is a function constant taking one argument. We can also
// make a function constant which uses both of the introduced sorts.
ctx += hoc"f:i>nat" //Takes a term of "i" and returns a term of "nat"
//in FirstSchema2.scala we continue with the introduction of predicates, theory
// axioms, proof names, and primitive recursive symbols.
}